
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Translation.ErgoNameResolve</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Translation.ErgoNameResolve" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Translation.ErgoNameResolve</h1>
<div class="coq">
<br/>
<div class="doc">Ergo is a language for expressing contract logic. </div>
<br/>
<h1> Abstract Syntax </h1>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html">ErgoSpec.Common.Utils.NamespaceContext</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html">ErgoSpec.Common.Utils.Ast</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.CTO.CTO.html">ErgoSpec.Common.CTO.CTO</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html">ErgoSpec.Common.Types.ErgoType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html">ErgoSpec.Ergo.Lang.Ergo</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Translation.CTOtoErgo.html">ErgoSpec.Translation.CTOtoErgo</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoNameResolution">ErgoNameResolution</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>) : (<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#dls">dls</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DNamespace">DNamespace</a></span> <span class="id">_</span> <span class="id">ns</span>' :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ns</span>', <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id">_</span> <span class="id">_</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id">tname</span> <span class="id">td</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ln</span> := <span class="id">td</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ln">ln</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ectxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_enums">namespace_ctxt_enums</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_is_enum">type_declaration_is_enum</a></span> <span class="id">td</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_type">type_declaration_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#update_namespace_context_enums">update_namespace_context_enums</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">ns</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_type_to_namespace_ctxt">add_type_to_namespace_ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ln">ln</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DStmt">DStmt</a></span> <span class="id">_</span> <span class="id">_</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DConstant">DConstant</a></span> <span class="id">_</span> <span class="id">ln</span> <span class="id">ta</span> <span class="id">cd</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">ns</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_constant_to_namespace_ctxt">add_constant_to_namespace_ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id">_</span> <span class="id">ln</span> <span class="id">fd</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">ns</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_function_to_namespace_ctxt">add_function_to_namespace_ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id">_</span> <span class="id">ln</span> <span class="id">_</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">ns</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_contract_to_namespace_ctxt">add_contract_to_namespace_ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DSetContract">DSetContract</a></span> <span class="id">_</span> <span class="id">ln</span> <span class="id">_</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id">rest</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_ctxt_of_ergo_module">namespace_ctxt_of_ergo_module</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">m</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_decls">namespace_ctxt_of_ergo_decls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_namespace">module_namespace</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_declarations">module_declarations</a></span>)).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_ctxt_of_ergo_modules">namespace_ctxt_of_ergo_modules</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">ml</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_module">namespace_ctxt_of_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ml">ml</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_ctxt_of_cto_packages">namespace_ctxt_of_cto_packages</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) (<span class="id">ctos</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.CTO.CTO.html#cto_package">cto_package</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">mls</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> <span class="id"><a href="ErgoSpec.Translation.CTOtoErgo.html#cto_package_to_ergo_module">cto_package_to_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctos">ctos</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_module">namespace_ctxt_of_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#mls">mls</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoNameResolution.ResolveImports">ResolveImports</a></span>.<br/>
<div class="doc">This applies imports </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="lookup_one_import">lookup_one_import</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ic</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#limport_decl">limport_decl</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ic">ic</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id">prov</span> <span class="id">ns</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_modules">namespace_ctxt_modules</a></span>) <span class="id">ns</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">tbl</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">tbl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#import_not_found_error">import_not_found_error</a></span> <span class="id">prov</span> <span class="id">ns</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id">prov</span> <span class="id">ns</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_modules">namespace_ctxt_modules</a></span>) <span class="id">ns</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">tbl</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">tbl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#empty_namespace_table">empty_namespace_table</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportName">ImportName</a></span> <span class="id">prov</span> <span class="id">ns</span> <span class="id">ln</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_modules">namespace_ctxt_modules</a></span>) <span class="id">ns</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">tbl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id">tbl</span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table_types">namespace_table_types</a></span>) <span class="id">ln</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#import_name_not_found_error">import_name_not_found_error</a></span> <span class="id">prov</span> <span class="id">ns</span> <span class="id">ln</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">an</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#one_type_to_namespace_table">one_type_to_namespace_table</a></span> <span class="id">ln</span> <span class="id">an</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#import_not_found_error">import_not_found_error</a></span> <span class="id">prov</span> <span class="id">ns</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_one_import">resolve_one_import</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ic</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#limport_decl">limport_decl</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">tbl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#mkNamespaceCtxt">mkNamespaceCtxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_modules">namespace_ctxt_modules</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_namespace">namespace_ctxt_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_current_module">namespace_ctxt_current_module</a></span>) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table_app">namespace_table_app</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_current_in_scope">namespace_ctxt_current_in_scope</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_enums">namespace_ctxt_enums</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_abstract">namespace_ctxt_abstract</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#lookup_one_import">lookup_one_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ic">ic</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_builtin_import">is_builtin_import</a></span> (<span class="id">ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#stdlib_namespace">stdlib_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ErgoNameResolution.ResolveImports">ResolveImports</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoNameResolution.NameResolution">NameResolution</a></span>.<br/>
<div class="doc">Name resolution for type declarations </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="resolve_ergo_type">resolve_ergo_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type">lrergo_type</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeNothing">ErgoTypeNothing</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeNothing">ErgoTypeNothing</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeUnit">ErgoTypeUnit</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeUnit">ErgoTypeUnit</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeString">ErgoTypeString</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeString">ErgoTypeString</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDouble">ErgoTypeDouble</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDouble">ErgoTypeDouble</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeLong">ErgoTypeLong</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeLong">ErgoTypeLong</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeInteger">ErgoTypeInteger</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeInteger">ErgoTypeInteger</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDateTime">ErgoTypeDateTime</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDateTime">ErgoTypeDateTime</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">prov</span> <span class="id">rn</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_type_name">resolve_type_name</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">rn</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">an</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#in_dec">in_dec</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeString">ErgoTypeString</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeOption">ErgoTypeOption</a></span> <span class="id">prov</span> <span class="id">t</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeOption">ErgoTypeOption</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeRecord">ErgoTypeRecord</a></span> <span class="id">prov</span> <span class="id">r</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">initial_map</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>))) <span class="id">r</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">lifted_map</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">t</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span>)) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#initial_map">initial_map</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeRecord">ErgoTypeRecord</a></span> <span class="id">prov</span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#lifted_map">lifted_map</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeArray">ErgoTypeArray</a></span> <span class="id">prov</span> <span class="id">t</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeArray">ErgoTypeArray</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeSum">ErgoTypeSum</a></span> <span class="id">prov</span> <span class="id">t1</span> <span class="id">t2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeSum">ErgoTypeSum</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">t1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">t2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_type_struct">resolve_ergo_type_struct</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type">lrergo_type</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>)) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">t</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span>)) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>))) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#t">t</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_type_annotation">resolve_type_annotation</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">en</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#relative_name">relative_name</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#en">en</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">rn</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_type_name">resolve_type_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">rn</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_extends">resolve_extends</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">en</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#rextends">rextends</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#aextends">aextends</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_type_annotation">resolve_type_annotation</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#en">en</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_type_signature">resolve_ergo_type_signature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sig</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_signature">lrergo_type_signature</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_signature">laergo_type_signature</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">params_types</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sig">sig</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_params">type_signature_params</a></span>)) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">output_type</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sig">sig</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_output">type_signature_output</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">out_ty</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">out_ty</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">emits_type</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sig">sig</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_emits">type_signature_emits</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">emits_ty</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">emits_ty</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sig">sig</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_annot">type_signature_annot</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#params_types">params_types</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#output_type">output_type</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#emits_type">emits_type</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_type_clauses">resolve_ergo_type_clauses</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">cls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_signature">lrergo_type_signature</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_signature">laergo_type_signature</a></span>)) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">r</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#r">r</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_signature">resolve_ergo_type_signature</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span>))) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#cls">cls</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_type_declaration_desc">resolve_ergo_type_declaration_desc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration_desc">lrergo_type_declaration_desc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration_desc">laergo_type_declaration_desc</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#d">d</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEnum">ErgoTypeEnum</a></span> <span class="id">l</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEnum">ErgoTypeEnum</a></span> <span class="id">l</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeTransaction">ErgoTypeTransaction</a></span> <span class="id">isabs</span> <span class="id">extends_name</span> <span class="id">ergo_type_struct</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeTransaction">ErgoTypeTransaction</a></span> <span class="id">isabs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_extends">resolve_extends</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">extends_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_struct</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span> <span class="id">isabs</span> <span class="id">extends_name</span> <span class="id">ergo_type_struct</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span> <span class="id">isabs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_extends">resolve_extends</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">extends_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_struct</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEvent">ErgoTypeEvent</a></span> <span class="id">isabs</span> <span class="id">extends_name</span> <span class="id">ergo_type_struct</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEvent">ErgoTypeEvent</a></span> <span class="id">isabs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_extends">resolve_extends</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">extends_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_struct</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAsset">ErgoTypeAsset</a></span> <span class="id">isabs</span> <span class="id">extends_name</span> <span class="id">ergo_type_struct</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAsset">ErgoTypeAsset</a></span> <span class="id">isabs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_extends">resolve_extends</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">extends_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_struct</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeParticipant">ErgoTypeParticipant</a></span> <span class="id">isabs</span> <span class="id">extends_name</span> <span class="id">ergo_type_struct</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeParticipant">ErgoTypeParticipant</a></span> <span class="id">isabs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_extends">resolve_extends</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">extends_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_struct">resolve_ergo_type_struct</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_struct</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeGlobal">ErgoTypeGlobal</a></span> <span class="id">ergo_type</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeGlobal">ErgoTypeGlobal</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeFunction">ErgoTypeFunction</a></span> <span class="id">ergo_type_signature</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeFunction">ErgoTypeFunction</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_signature">resolve_ergo_type_signature</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ergo_type_signature</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeContract">ErgoTypeContract</a></span> <span class="id">template_type</span> <span class="id">state_type</span> <span class="id">clauses_sigs</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeContract">ErgoTypeContract</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">template_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">state_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_clauses">resolve_ergo_type_clauses</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">clauses_sigs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_type_declaration">resolve_ergo_type_declaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">module_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decl</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#abstract_ctxt">abstract_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration">lrergo_type_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#abstract_ctxt">abstract_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">ectxt</span>,<span class="id">actxt</span>,<span class="id">decl</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">name</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ectxt</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_is_enum">type_declaration_is_enum</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_type">type_declaration_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#name">name</a></span> :: <span class="id">ectxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id">ectxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actxt</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_is_abstract">type_declaration_is_abstract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_type">type_declaration_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#name">name</a></span> :: <span class="id">actxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id">actxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">edecl_desc</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_declaration_desc">resolve_ergo_type_declaration_desc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_annot">type_declaration_annot</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_type">type_declaration_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">k</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#actxt">actxt</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeDeclaration">mkErgoTypeDeclaration</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_annot">type_declaration_annot</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#name">name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#k">k</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#edecl_desc">edecl_desc</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_pattern">resolve_ergo_pattern</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#lrergo_pattern">lrergo_pattern</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#laergo_pattern">laergo_pattern</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#p">p</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseData">CaseData</a></span> <span class="id">prov</span> <span class="id">d</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseData">CaseData</a></span> <span class="id">prov</span> <span class="id">d</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseWildcard">CaseWildcard</a></span> <span class="id">prov</span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseWildcard">CaseWildcard</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_type_annotation">resolve_type_annotation</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLet">CaseLet</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLet">CaseLet</a></span> <span class="id">prov</span> <span class="id">v</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_type_annotation">resolve_type_annotation</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLetOption">CaseLetOption</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLetOption">CaseLetOption</a></span> <span class="id">prov</span> <span class="id">v</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_type_annotation">resolve_type_annotation</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
<div class="doc">Name resolution for expressions </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="resolve_ergo_expr">resolve_ergo_expr</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisClause">EThisClause</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisClause">EThisClause</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisState">EThisState</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisState">EThisState</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id">v</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id">v</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id">d</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id">d</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENone">ENone</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENone">ENone</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ESome">ESome</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ESome">ESome</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EArray">EArray</a></span> <span class="id">prov</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EArray">EArray</a></span> <span class="id">prov</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id">u</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id">u</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EBinaryOp">EBinaryOp</a></span> <span class="id">prov</span> <span class="id">b</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EBinaryOp">EBinaryOp</a></span> <span class="id">prov</span> <span class="id">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">e2</span> <span class="id">e3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rta</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">ta</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">v</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rta">rta</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENew">ENew</a></span> <span class="id">prov</span> <span class="id">cr</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rcr</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_type_name">resolve_type_name</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">cr</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_rec</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">att</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>))) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">attname</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#att">att</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#att">att</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="kwd">fun</span> <span class="id">acc</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#attname">attname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENew">ENew</a></span> <span class="id">prov</span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rcr">rcr</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_rec">init_rec</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ERecord">ERecord</a></span> <span class="id">prov</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_rec</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">att</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>))) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">attname</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#att">att</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#att">att</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="kwd">fun</span> <span class="id">acc</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#attname">attname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ERecord">ERecord</a></span> <span class="id">prov</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_rec">init_rec</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id">prov</span> <span class="id">fname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rfname</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_function_name">resolve_function_name</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>,<span class="id">fname</span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id">prov</span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rfname">rfname</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span> <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rgname</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_contract_name">resolve_contract_name</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">gname</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span> <span class="id">prov</span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rgname">rgname</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">fname</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id">e0</span> <span class="id">ecases</span> <span class="id">edefault</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ec0</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e0</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">eccases</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> <span class="id">acc</span> (<span class="id">ecase</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#lrergo_pattern">lrergo_pattern</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">pcase</span>, <span class="id">pe</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ecase">ecase</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">apcase</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_pattern">resolve_ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#pcase">pcase</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">apcase</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#apcase">apcase</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#pe">pe</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#apcase">apcase</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id">ecases</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ecdefault</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">edefault</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ec0</span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">eccases</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#laergo_pattern">laergo_pattern</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ecdefault</span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ec0">ec0</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#eccases">eccases</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ecdefault">ecdefault</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ecdefault">ecdefault</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#eccases">eccases</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ec0">ec0</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span> <span class="id">foreachs</span> <span class="id">econd</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">re2</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e2</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">recond</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">econd</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">econd</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">econd</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_e</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">foreach</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">v</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#foreach">foreach</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#foreach">foreach</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="kwd">fun</span> <span class="id">acc</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#v">v</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_e">init_e</a></span> <span class="id">foreachs</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#recond">recond</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#re2">re2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<div class="doc">Name resolution for statements </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="resolve_ergo_stmt">resolve_ergo_stmt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_stmt">lrergo_stmt</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_stmt">laergo_stmt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SFunReturn">SFunReturn</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SFunReturn">SFunReturn</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SThrow">SThrow</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt;  <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SThrow">SThrow</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SCallClause">SCallClause</a></span> <span class="id">prov</span> <span class="id">e0</span> <span class="id">fname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_expr">lrergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SCallClause">SCallClause</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e0</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">fname</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SSetState">SSetState</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SSetState">SSetState</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEmit">SEmit</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEmit">SEmit</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SLet">SLet</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rta</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">ta</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SLet">SLet</a></span> <span class="id">prov</span> <span class="id">v</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rta">rta</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SIf">SIf</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> <span class="id">s3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SIf">SIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEnforce">SEnforce</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">os2</span> <span class="id">s3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rs2</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">os2</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">s2</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEnforce">SEnforce</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rs2">rs2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">s3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SMatch">SMatch</a></span> <span class="id">prov</span> <span class="id">e0</span> <span class="id">scases</span> <span class="id">sdefault</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ec0</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e0</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">sccases</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> <span class="id">acc</span> (<span class="id">scase</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#lrergo_pattern">lrergo_pattern</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_stmt">lrergo_stmt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">pcase</span>, <span class="id">pe</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#scase">scase</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">apcase</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_pattern">resolve_ergo_pattern</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#pcase">pcase</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">apcase</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#apcase">apcase</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#pe">pe</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#apcase">apcase</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#proc_one">proc_one</a></span> <span class="id">scases</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">scdefault</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">sdefault</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ec0</span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sccases</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#laergo_pattern">laergo_pattern</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_stmt">laergo_stmt</a></span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">scdefault</span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_stmt">laergo_stmt</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SMatch">SMatch</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ec0">ec0</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sccases">sccases</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#scdefault">scdefault</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#scdefault">scdefault</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#sccases">sccases</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ec0">ec0</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<div class="doc">Name resolution for lambdas </div>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_function">resolve_ergo_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">module_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_function">lrergo_function</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_function">laergo_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">prov</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_annot">function_annot</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rbody</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_body">function_body</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">body</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">body</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkFunc">mkFunc</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_signature">resolve_ergo_type_signature</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_sig">function_sig</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rbody">rbody</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_clause">resolve_ergo_clause</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">module_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_clause">ergo_clause</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_clause">laergo_clause</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">prov</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_annot">clause_annot</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rcname</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_name">clause_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rbody</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_body">clause_body</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">body</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">body</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkClause">mkClause</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rcname">rcname</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_signature">resolve_ergo_type_signature</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_sig">clause_sig</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rbody">rbody</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_clauses">resolve_ergo_clauses</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">module_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">cl</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_clause">ergo_clause</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_clause">laergo_clause</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_clause">resolve_ergo_clause</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#cl">cl</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_contract">resolve_ergo_contract</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">module_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ectxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tbl</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_contract">lrergo_contract</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_contract">laergo_contract</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">prov</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_annot">contract_annot</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rtemplate</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_template">contract_template</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rstate</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_state">contract_state</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">state</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">state</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkContract">mkContract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#prov">prov</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rtemplate">rtemplate</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rstate">rstate</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_clauses">resolve_ergo_clauses</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_clauses">contract_clauses</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_declaration">resolve_ergo_declaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_declaration">laergo_declaration</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">module_ns</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_namespace">namespace_ctxt_namespace</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ectxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_enums">namespace_ctxt_enums</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_abstract">namespace_ctxt_abstract</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">tbl</span> : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_table">namespace_table</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_current_in_scope">namespace_ctxt_current_in_scope</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#d">d</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DNamespace">DNamespace</a></span> <span class="id">prov</span> <span class="id">ns</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DNamespace">DNamespace</a></span> <span class="id">prov</span> <span class="id">ns</span>, <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#local_namespace_scope">local_namespace_scope</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id">ns</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id">prov</span> <span class="id">id</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id">prov</span> <span class="id">id</span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>)) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_one_import">resolve_one_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id">id</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id">prov</span> <span class="id">td</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ln</span> := <span class="id">td</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ln">ln</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_type_to_namespace_ctxt_current">add_type_to_namespace_ctxt_current</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ln">ln</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#enum_ctxt">enum_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#abstract_ctxt">abstract_ctxt</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">ectxt</span>,<span class="id">actxt</span>,<span class="id">x</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#xy">xy</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#update_namespace_context_enums">update_namespace_context_enums</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#update_namespace_context_abstract">update_namespace_context_abstract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#actxt">actxt</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id">prov</span> <span class="id">x</span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type_declaration">resolve_ergo_type_declaration</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#actxt">actxt</a></span>, <span class="id">td</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DStmt">DStmt</a></span> <span class="id">prov</span> <span class="id">st</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DStmt">DStmt</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>)) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_stmt">resolve_ergo_stmt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">st</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DConstant">DConstant</a></span> <span class="id">prov</span> <span class="id">ln</span> <span class="id">ta</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rta</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">ta</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">ta</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_type">resolve_ergo_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_constant_to_namespace_ctxt_current">add_constant_to_namespace_ctxt_current</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">ta</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DConstant">DConstant</a></span> <span class="id">prov</span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ta">ta</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#rta">rta</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id">prov</span> <span class="id">ln</span> <span class="id">fd</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_function_to_namespace_ctxt_current">add_function_to_namespace_ctxt_current</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>)) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_function">resolve_ergo_function</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">fd</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id">prov</span> <span class="id">ln</span> <span class="id">c</span>  =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">an</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id">ln</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#add_contract_to_namespace_ctxt_current">add_contract_to_namespace_ctxt_current</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id">ln</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>)) (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_contract">resolve_ergo_contract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">c</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DSetContract">DSetContract</a></span> <span class="id">prov</span> <span class="id">rn</span> <span class="id">e1</span>  =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">an</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DSetContract">DSetContract</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#an">an</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_expr">resolve_ergo_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ectxt">ectxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">e1</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#resolve_contract_name">resolve_contract_name</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#tbl">tbl</a></span> <span class="id">rn</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_declarations">resolve_ergo_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_declaration">ergo_declaration</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_context_fold_left">elift_context_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_declaration">resolve_ergo_declaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="silently_resolve_ergo_declarations">silently_resolve_ergo_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_declarations">resolve_ergo_declarations</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ErgoNameResolution.NameResolution">NameResolution</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoNameResolution.Top">Top</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="init_namespace_ctxt">init_namespace_ctxt</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#empty_namespace_ctxt">empty_namespace_ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#no_namespace">no_namespace</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="patch_cto_imports">patch_cto_imports</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#is_builtin_import">is_builtin_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span>)) :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="patch_ergo_imports">patch_ergo_imports</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt_ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_declaration">lrergo_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#is_builtin_import">is_builtin_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#app">app</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span>) :: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#stdlib_namespace">stdlib_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt_ns">ctxt_ns</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#decls">decls</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="new_cto_package_namespace">new_cto_package_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">m</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#is_builtin_import">is_builtin_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">builtin_cto_imports</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#new_namespace_scope">new_namespace_scope</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_module">namespace_ctxt_of_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span> <span class="kwd">in</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#silently_resolve_ergo_declarations">silently_resolve_ergo_declarations</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#builtin_cto_imports">builtin_cto_imports</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="new_ergo_module_namespace">new_ergo_module_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#is_builtin_import">is_builtin_import</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">builtin_cto_imports</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#stdlib_namespace">stdlib_namespace</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportSelf">ImportSelf</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#new_namespace_scope">new_namespace_scope</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ns">ns</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#silently_resolve_ergo_declarations">silently_resolve_ergo_declarations</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#builtin_cto_imports">builtin_cto_imports</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_cto_package">resolve_cto_package</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">cto</span>:<span class="id"><a href="ErgoSpec.Common.CTO.CTO.html#lrcto_package">lrcto_package</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">m</span> := <span class="id"><a href="ErgoSpec.Translation.CTOtoErgo.html#cto_package_to_ergo_module">cto_package_to_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#cto">cto</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">module_ns</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_namespace">module_namespace</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#new_namespace_scope">new_namespace_scope</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_ergo_module">namespace_ctxt_of_ergo_module</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span> <span class="kwd">in</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">declarations</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_declarations">module_declarations</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt_ns</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_namespace">namespace_ctxt_namespace</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">nc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_annot">module_annot</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_file">module_file</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#nc">nc</a></span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#nc">nc</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_declarations">resolve_ergo_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#patch_cto_imports">patch_cto_imports</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#declarations">declarations</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_module">resolve_ergo_module</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">m</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">module_ns</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_namespace">module_namespace</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#new_namespace_scope">new_namespace_scope</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">declarations</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_declarations">module_declarations</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt_ns</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_namespace">namespace_ctxt_namespace</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">nc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_annot">module_annot</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#m">m</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_file">module_file</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#nc">nc</a></span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#nc">nc</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_declarations">resolve_ergo_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#patch_ergo_imports">patch_ergo_imports</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#module_ns">module_ns</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#declarations">declarations</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_ergo_modules">resolve_ergo_modules</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ml</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_context_fold_left">elift_context_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_module">resolve_ergo_module</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ml">ml</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="resolve_cto_packages">resolve_cto_packages</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctos</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.CTO.CTO.html#lrcto_package">lrcto_package</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#namespace_ctxt_of_cto_packages">namespace_ctxt_of_cto_packages</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctos">ctos</a></span> <span class="kwd">in</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_context_fold_left">elift_context_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_cto_package">resolve_cto_package</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctos">ctos</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="split_ctos_and_ergos">split_ctos_and_ergos</a></span> (<span class="id">inputs</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_input">lrergo_input</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.CTO.CTO.html#lrcto_package">lrcto_package</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#inputs">inputs</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#InputCTO">InputCTO</a></span> <span class="id">cto</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">ctos</span>', <span class="id">rest</span>', <span class="id">p</span>') := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#split_ctos_and_ergos">split_ctos_and_ergos</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">cto</span> :: <span class="id">ctos</span>', <span class="id">rest</span>', <span class="id">p</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#InputErgo">InputErgo</a></span> <span class="id">ml</span> :: <span class="id">rest</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">ctos</span>', <span class="id">rest</span>', <span class="id">p</span>') := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#split_ctos_and_ergos">split_ctos_and_ergos</a></span> <span class="id">rest</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">p</span>' <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#is_builtin_import">is_builtin_import</a></span> <span class="id">ml</span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_namespace">module_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id">ctos</span>', <span class="id">ml</span> :: <span class="id">rest</span>', <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> (<span class="id">ctos</span>', <span class="id">rest</span>', <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">ml</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">_</span> =&gt; (<span class="id">ctos</span>', <span class="id">ml</span> :: <span class="id">rest</span>', <span class="id">p</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ErgoNameResolution.Top">Top</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoNameResolution.Examples">Examples</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_typed1">ergo_typed1</a></span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration">lrergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeDeclaration">mkErgoTypeDeclaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">c1</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">a</span>", <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::("<span class="id">b</span>", (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, "<span class="id">c3</span>")))::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_typed2">ergo_typed2</a></span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration">lrergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeDeclaration">mkErgoTypeDeclaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">c2</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">c</span>", <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::("<span class="id">d</span>", (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, "<span class="id">c1</span>")))::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_funcd1">ergo_funcd1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_function">lrergo_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkFunc">mkFunc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_funcd2">ergo_funcd2</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_function">lrergo_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkFunc">mkFunc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>" <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_clause2">ergo_clause2</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_clause">lrergo_clause</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkClause">mkClause</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">addFee2</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>" <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>))).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_contractd1">ergo_contractd1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_contract">lrergo_contract</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkContract">mkContract</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_clause2">ergo_clause2</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_module1">ergo_module1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;""<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">n1</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#ImportAll">ImportAll</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">n2</span>")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>" <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_funcd1">ergo_funcd1</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">MyContract</span>" <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_contractd1">ergo_contractd1</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_typed1">ergo_typed1</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_typed2">ergo_typed2</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_typed3">ergo_typed3</a></span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration">lrergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeDeclaration">mkErgoTypeDeclaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">c3</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">a</span>", <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::("<span class="id">b</span>", <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeString">ErgoTypeString</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_typed_top">ergo_typed_top</a></span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lrergo_type_declaration">lrergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeDeclaration">mkErgoTypeDeclaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">top</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeGlobal">ErgoTypeGlobal</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_module2">ergo_module2</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "" "<span class="id">n2</span>" (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_typed3">ergo_typed3</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_hl">ergo_hl</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "" <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#hyperledger_namespace">hyperledger_namespace</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_typed_top">ergo_typed_top</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_stdlib">ergo_stdlib</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkModule">mkModule</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "" <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#stdlib_namespace">stdlib_namespace</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_typed_top">ergo_typed_top</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ml1">ml1</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_hl">ergo_hl</a></span> :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_stdlib">ergo_stdlib</a></span> :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_module2">ergo_module2</a></span> :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_module1">ergo_module1</a></span> :: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="aml1">aml1</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_modules">resolve_ergo_modules</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#empty_namespace_ctxt">empty_namespace_ctxt</a></span> "<span class="id">TEST</span>") <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ml1">ml1</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ml2">ml2</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#lrergo_module">lrergo_module</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_hl">ergo_hl</a></span> :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_stdlib">ergo_stdlib</a></span> :: <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_module2">ergo_module2</a></span> :: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="aml2">aml2</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_modules">resolve_ergo_modules</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#empty_namespace_ctxt">empty_namespace_ctxt</a></span> "<span class="id">TEST</span>") <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ml2">ml2</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="aml3">aml3</a></span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">mc</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#resolve_ergo_module">resolve_ergo_module</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#mc">mc</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ergo_module1">ergo_module1</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#aml2">aml2</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ErgoNameResolution.Examples">Examples</a></span>.<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#ErgoNameResolution">ErgoNameResolution</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
